Inference at * 1 
Iof proof for Lemma nat ind:



1. P : {k}
2. P(0)
3. i:. P(i - 1)  P(i)
4. j : 
  P(j) 

latex

 by InteriorProof NatInd 4 

latex

 1: .....basecase..... NILNIL

 1: 3. i:. P(i - 1)  P(i)
 1:   P(0)
 2: .....upcase..... NILNIL

 2: 4. j : 
 2: 5. 0 < j
 2: 6. P(j - 1)
 2:   P(j)
 .

Definitions	False, A, A  B, i  j , P  Q, t  T, x:A. B(x), ,
Lemmas	ge wf, nat properties